COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	proof? 
C00009 00003
C00011 ENDMK
C⊗;
proof? 
* LISPX started.
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 12. ∀U.SEXP U
    ctxt: (1 11)   deps: NIL

* 13. ∀X U.LISTP CONS(X,U)
    ctxt: (1 2 6 10)   deps: NIL

* 14. ∀X U.LISTP X:U
    ctxt: (1 2 7 10)   deps: NIL

* 15. ∀U.NULL U≡U=NNIL
    ctxt: (1 5 9)   deps: NIL

* 16. ∀X U.¬NULL CONS(X,U)
    ctxt: (1 2 6 9)   deps: NIL

* 17. ∀X U.¬NULL X:U
    ctxt: (1 2 7 9)   deps: NIL

* 18. ∀X U.CAR CONS(X,U)=X
    ctxt: (1 2 6 8)   deps: NIL

* 19. ∀X U.CAR (X:U)=X
    ctxt: (1 2 7 8)   deps: NIL

* 20. ∀X U.CDR CONS(X,U)=U
    ctxt: (1 2 6 8)   deps: NIL

* 21. ∀X U.CDR (X:U)=U
    ctxt: (1 2 7 8)   deps: NIL

* 22. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))
    ctxt: (1 2 4 5 6)   deps: NIL

* compute-type: PHI does not apply in PHI(X,:,U)
in the current context PHI has type GROUND→TRUTHVAL
* 
* 24. ∀U V.LISTP U*V
    ctxt: (1 10 23)   deps: NIL

* 25. ∀U V.U*V=IF NULL U THEN V ELSE CONS(CAR U,CDR U*V)
    ctxt: (1 6 8 9 23)   deps: NIL

* 26. ∀U V.U*V=IF NULL U THEN V ELSE CAR U:(CDR U*V)
    ctxt: (1 7 8 9 23)   deps: NIL

* 
* 
* 29. ∀X.LISTP LIST(X)
    ctxt: (2 10 28)   deps: NIL

* 30. ∀X.LIST(X)=CONS(X,NNIL)
    ctxt: (2 5 6 28)   deps: NIL

* 31. ∀X Y.LISTP LIST(X,Y)
    ctxt: (2 10 28)   deps: NIL

* 32. ∀X Y.LIST(X,Y)=CONS(X,LIST(Y))
    ctxt: (2 6 28)   deps: NIL

* 33. ∀X Y Z.LISTP LIST(X,Y,Z)
    ctxt: (2 10 28)   deps: NIL

* 34. ∀X Y Z.LIST(X,Y,Z)=CONS(X,LIST(Y,Z))
    ctxt: (2 6 28)   deps: NIL

* 35. ∀U.LISTP REVERSE U
    ctxt: (1 10 27)   deps: NIL

* 36. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)
    ctxt: (1 5 8 9 23 27 28)   deps: NIL

* 37. ∀U V W.(U*V)*W=U*(V*W)
    ctxt: (1 23)   deps: NIL

* 38. ∀X U V.CONS(X,U*V)=CONS(X,U)*V
    ctxt: (1 2 6 23)   deps: NIL

* 39. ∀U V.REVERSE (U*V)=REVERSE V*REVERSE U
    ctxt: (1 23 27)   deps: NIL

* 
;;; lispx.lsp[f81,jmc]	ekl axioms for lisp

(proof lispx)

(DECL (U u0 u1 u2 u3 v v0 v1 v2 v3 W w0 w1 w2 w3) |ground| variable listp)

(DECL (X Y Z) |GROUND| VARIABLE sEXP)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONsTANT LIsTp)

(DECL (CONs) |GROUND⊗GROUND→GROUND| CONsTANT)

(DECL (:) |GROUND⊗GROUND→GROUND| CONsTANT NIL INFIX 850)

(DECL (CAR CDR) |GROUND→GROUND| CONsTANT nil unary 950)

(DECL (NULL) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(DECL (LIsTp) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(DECL (sEXP) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(AXIOM |∀U.sEXP U |)

(AXIOM |∀X U.LISTP CONS(X,U)|)

(AXIOM |∀X U.LISTP X:U |)

(AXIOM |∀U.NULL U ≡ U=NNIL|)

(AXIOM |∀X U.¬NULL CONs(X,U)|)

(AXIOM |∀X U.¬NULL X:U|)

(AXIOM |∀X U.CAR CONs(X,U) =X|)

(AXIOM |∀X U.CAR (X : U) = X|)

(AXIOM |∀X U.CDR CONs(X,U) = U|)

(AXIOM |∀X U.CDR (X:U) = U|)

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONs(X,U)))⊃(∀U.PHI(U))|)

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X:U))⊃(∀U.PHI(U))|)

;;; Common defined functions

(DECL (*) |GROUND⊗GROUND→GROUND| CONsTANT NIL INFIX 840)

(axiom |∀u v.listp(u*v)|)

(AXIOM |∀U V.(U*V)=IF NULL(U) THEN V ELsE CONs(CAR(U),CDR(U)*V)|)

(AXIOM |∀U V.(U*V)=IF NULL(U) THEN V ELsE CAR U : (CDR U *V)|)

(decl (reverse) |ground→ground| constant nil unary 950)

(decl list |ground* → ground| functional)

(axiom |∀x.listp(list(x))|)

(axiom |∀x.list(x) = cons(x,nnil)|)

(axiom |∀x y.listp(list(x,y))|)

(axiom |∀x y.list(x,y) = cons(x,list(y))|)

(axiom |∀x y z.listp(list(x,y,z))|)

(axiom |∀x y z.list(x,y,z) = cons(x,list(y,z))|)

(axiom |∀u.listp(reverse(u))|)

(axiom |∀u.reverse(u) = if null(u) then nnil
else reverse(cdr(u)) * list(car(u))|)

;;; theorems taken as axioms for further proofs

(axiom |∀u v w.(u*v)*w = u*(v*w)|)

(axiom |∀x u v.cons(x,u*v) = cons(x,u)*v|)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)